COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE OPCONST APP 2[L←400 R←395]
C00003 ENDMK
C⊗;
DECLARE OPCONST APP 2[L←400 R←395];

AXIOM APPEND:
	∀x y.(x APP y = IF x = NILL THEN y ELSE CONS(CAR x, CDR x APP y))
;;

DECLARE OPCONST FLAT 2;

AXIOM FLAT:
	∀x u.(FLAT(x,u) = IF ATOM x THEN CONS(x,u) ELSE FLAT(CAR x,FLAT(CDR x,u)))
;;

DECLARE OPCONST ALT 1[R←600];

AXIOM ALT:
∀u.(ALT(u)=(IF (u=NILL ∨ CDR(u)=NILL) THEN u ELSE CONS(CAR u,ALT(CDR(CDR u)))))
;;